T:Type, l1, l2, l3:T List.
l1  l2 @ l3  l1  l2  (l:T List. 0<||l|| & l1 = (l2 @ l) & l  l3) 

latex

Definitions	t  T, l1  l2, P & Q, x:A. B(x), P  Q, P  Q, x:A. B(x), as @ bs, Prop, ||as||, P  Q, P  Q, A & B, ij, {T}, False, b, hd(l), A, AB, tl(l)
Lemmas	tl wf, ge wf, hd wf, iseg append, or functionality wrt iff, cons iseg, iseg nil, length cons, non neg length, nil iseg, length wf1, append wf, iseg wf